package model.logic;

import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;

/**
 * A Conjunction is a <tt>List</tt> of <tt>Propositions</tt> linked by logical and. 
 *  
 * @author Marius Tempelmeier
 *
 */
public class Conjunction {
	
	/**
	 * conjuncted prepositions. 
	 */
	private final List<Proposition> propositions;

	public Conjunction(List<Proposition> propositions) {
		this.propositions = propositions;
	}
	
	public Conjunction() {
		this.propositions = new ArrayList<Proposition>();
	}
	
	/**
	 * Adds <tt>Proposition</tt> p to this.  
	 * @param p <tt>Proposition</tt> to be added
	 */
	public void addProposition(Proposition p) {
			this.propositions.add(p);
	}

	/**
	 * Checks if <tt>c</tt> is derivable by this. 
	 * @param c Conjunction to be checked
	 * @return true <=> this |- <tt>c</tt>
	 */
	public boolean derives(Conjunction c) {
		return c.isDerivableBy(this);
	}
	
	/**
	 * Checks if this is derivable by <tt>c</tt>.   
	 * @param c Conjunction to be checked
	 * @return true <=> this -| <tt>c</tt>
	 */
	private boolean isDerivableBy(Conjunction c) {
		final Iterator<Proposition> i = this.propositions.iterator();
		while (i.hasNext()) {
			Proposition current = i.next();
			if (!c.containsDerivingProposition(current)) {
				return false;
			}
		}
		return true; 
	}
	
	/**
	 * Checks if this contains a <tt>Proposition</tt> which derives <tt>derivedProp</tt>. 
	 * @param derivedProp <tt>Proposition</tt> to be checked
	 * @return true <=> this contains a <tt>Proposition</tt> <tt>p</tt> : <tt>p</tt> |- <tt>derivedProp</tt>
	 */
	public boolean containsDerivingProposition(Proposition derivedProp) {
		Iterator<Proposition> i = this.propositions.iterator();
		while (i.hasNext()) {
			if (i.next().derives(derivedProp)) {
				return true;
			}
		}
		return false;
	}
}
